T:Type, L:(T List). sublist(T; []; L)  True 

latex

Definitions	suptype(S; T), subtype(S; T), , False, A, A  B, lelt(i; j; k), Y, ||as||, int_seg(i; j), x:A. B(x), prop{i:l}, t  T, P  Q, P  Q, P  Q, True, sublist(T; L1; L2), P  Q, x:A. B(x), increasing(f; k)
Lemmas	true wf, select wf, length wf2, increasing wf, int seg wf, le wf, length wf1, sublist wf